es:ES, e:E, l:IdLnk, L:E List. rcvs from e on l = L  es-receives(es;e;l) = L 

latex

Definitions	t  T, x:A. B(x), P & Q, A & B, x:AB(x), x:AB(x), P  Q, P  Q, lnk(e), IdLnk, s = t, sender(e), E, isrcv(e), b, Type, Prop, (x  l), P  Q, es-receives(es;e;l), l-ordered(T;x,y.R(x;y);L), loc-ordered(es;L), rcvs from e on l = L, ES, type List
Lemmas	es-rcv-from wf, event system wf, loc-ordered-equality, iff functionality wrt iff, member-es-receives, es-receives wf, l member wf, assert wf, es-isrcv wf, es-E wf, es-sender wf, IdLnk wf, es-lnk wf, loc-ordered-es-receives